Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a__a  → a__c
2:    a__b  → a__c
3:    a__c  → e
4:    a__k  → l
5:    a__d  → m
6:    a__a  → a__d
7:    a__b  → a__d
8:    a__c  → l
9:    a__k  → m
10:    a__A  → a__h(a__f(a__a),a__f(a__b))
11:    a__h(X,X)  → a__g(mark(X),mark(X),a__f(a__k))
12:    a__g(d,X,X)  → a__A
13:    a__f(X)  → a__z(mark(X),X)
14:    a__z(e,X)  → mark(X)
15:    mark(A)  → a__A
16:    mark(a)  → a__a
17:    mark(b)  → a__b
18:    mark(c)  → a__c
19:    mark(d)  → a__d
20:    mark(k)  → a__k
21:    mark(z(X1,X2))  → a__z(mark(X1),X2)
22:    mark(f(X))  → a__f(mark(X))
23:    mark(h(X1,X2))  → a__h(mark(X1),mark(X2))
24:    mark(g(X1,X2,X3))  → a__g(mark(X1),mark(X2),mark(X3))
25:    mark(e)  → e
26:    mark(l)  → l
27:    mark(m)  → m
28:    a__A  → A
29:    a__a  → a
30:    a__b  → b
31:    a__c  → c
32:    a__d  → d
33:    a__k  → k
34:    a__z(X1,X2)  → z(X1,X2)
35:    a__f(X)  → f(X)
36:    a__h(X1,X2)  → h(X1,X2)
37:    a__g(X1,X2,X3)  → g(X1,X2,X3)
There are 34 dependency pairs:
38:    A__A  → A__C
39:    A__B  → A__C
40:    A__A  → A__D
41:    A__B  → A__D
42:    A__A  → A__H(a__f(a__a),a__f(a__b))
43:    A__A  → A__F(a__a)
44:    A__A  → A__A
45:    A__A  → A__F(a__b)
46:    A__A  → A__B
47:    A__H(X,X)  → A__G(mark(X),mark(X),a__f(a__k))
48:    A__H(X,X)  → MARK(X)
49:    A__H(X,X)  → A__F(a__k)
50:    A__H(X,X)  → A__K
51:    A__G(d,X,X)  → A__A
52:    A__F(X)  → A__Z(mark(X),X)
53:    A__F(X)  → MARK(X)
54:    A__Z(e,X)  → MARK(X)
55:    MARK(A)  → A__A
56:    MARK(a)  → A__A
57:    MARK(b)  → A__B
58:    MARK(c)  → A__C
59:    MARK(d)  → A__D
60:    MARK(k)  → A__K
61:    MARK(z(X1,X2))  → A__Z(mark(X1),X2)
62:    MARK(z(X1,X2))  → MARK(X1)
63:    MARK(f(X))  → A__F(mark(X))
64:    MARK(f(X))  → MARK(X)
65:    MARK(h(X1,X2))  → A__H(mark(X1),mark(X2))
66:    MARK(h(X1,X2))  → MARK(X1)
67:    MARK(h(X1,X2))  → MARK(X2)
68:    MARK(g(X1,X2,X3))  → A__G(mark(X1),mark(X2),mark(X3))
69:    MARK(g(X1,X2,X3))  → MARK(X1)
70:    MARK(g(X1,X2,X3))  → MARK(X2)
71:    MARK(g(X1,X2,X3))  → MARK(X3)
The approximated dependency graph contains one SCC: {42,43,45,47-49,51-55,61-71}.
Tyrolean Termination Tool  (10.09 seconds)   ---  May 3, 2006